home *** CD-ROM | disk | FTP | other *** search
/ TeX 1995 July / TeX CD-ROM July 1995 (Disc 1)(Walnut Creek)(1995).ISO / macros / latex209 / contrib / oz / oz.sty < prev    next >
Text File  |  1991-08-08  |  42KB  |  1,293 lines

  1. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  2. %
  3. % oz.sty
  4. %
  5. \message{`OZ Macros' <9 Nov 90>}
  6. %
  7. %    This document is organised as follows:
  8. %
  9. %    SECTION 1    Z FONTS
  10. %    SECTION 2    Z SYMBOLS
  11. %    SECTION 3    Z ENVIRONMENTS
  12. %
  13. % Modification History:
  14. %
  15. %               The original zed.sty file was written by Mike Spivey.
  16. %               These macros have been extensively modified to
  17. %               include extra symbols and environments for Object-Z
  18. %               and now have little resemblence to the original macros.
  19. %               Mike Spivey has also extended his macros along
  20. %               different lines for Z - the latest version of macros
  21. %               are called fuzz.sty and come with a syntax checker for Z.
  22. %               They can be purchased for a small fee from:
  23. %                       mike@prg.oxford.ac.uk
  24. %
  25. %        87    original zed.sty file - Mike Spivey
  26. %        88    modified to include extra symbols and environments - Paul King
  27. %        88    modified to include macros for UQ editor - Ray Neucom
  28. %    May 89    modified to include object-oriented constructs - PK
  29. %    Jun 89    modified to automatically change Z symbol size - PK
  30. % 27 Jul 89    removed spurious space from \@setsize - PK
  31. %  3 Aug 89    adjust style of equation number field - PK
  32. % 24 Aug 89     add optional field to topline and zedline for proofs - PK
  33. % 15 Sep 89     added extra qed symbols, updated classcom and comment - PK
  34. % 25 Sep 89    renamed z@[bB]ig to z[bB]ig and changed temporal symbols - PK
  35. % 30 Sep 89    added \znewpage, \Infrule, removed space above state box - PK
  36. % 12 Mar 90    changed \@setsize to work better for double-spaced text - PK
  37. % 31 Mar 90    added definition for @ and \bool and redefined `;' - PK
  38. %  9 May 90    changed \sdef to \varsdef, \sdef & \defs to Spivey's latest - PK
  39. % 27 May 90    added \c{n}{text} - a tab like \t{n} with text at left - PK
  40. % 29 May 90    added `corners' to boxes and \zedcornerheight - PK
  41. % 11 Jul 90    added \rename*[y/x] and \zseq \zset ..., changed \zeq \zimp - PK
  42. %  2 Aug 90     added subseq - PK
  43. %  9 Nov 90    changed \M to hopefully interact better with spacing - PK
  44. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  45. % Please post any updates that you may make to this file to:
  46. %    Paul King -- ACSnet: king@batserver.cs.uq.oz.au
  47. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  48. %
  49. %    SECTION 1    Z FONTS
  50. %
  51. % The AMS extra symbol fonts are loaded.
  52. %    Note: msxm and msym sometimes called euxm and euym respectively
  53. %       NOTE: the new AMSFONTS 2.0 call these fonts msam and msbm repectively
  54. %       (the fonts below need to be renamed if you want to use the new fonts)
  55. %
  56. \font\fivmsx=msxm5            \font\fivmsy=msym5
  57. \font\sixmsx=msxm6            \font\sixmsy=msym6
  58. \font\sevmsx=msxm7            \font\sevmsy=msym7
  59. \font\egtmsx=msxm8            \font\egtmsy=msym8
  60. \font\ninmsx=msxm9            \font\ninmsy=msym9
  61. \font\tenmsx=msxm10            \font\tenmsy=msym10
  62. \font\elvmsx=msxm10 \@halfmag        \font\elvmsy=msym10 \@halfmag
  63. \font\twlmsx=msxm10 \@magscale1        \font\twlmsy=msym10 \@magscale1
  64. \font\frtnmsx=msxm10 \@magscale2    \font\frtnmsy=msym10 \@magscale2
  65. \font\svtnmsx=msxm10 \@magscale3    \font\svtnmsy=msym10 \@magscale3
  66. \font\twtymsx=msxm10 \@magscale4    \font\twtymsy=msym10 \@magscale4
  67. \font\twfvmsx=msxm10 \@magscale5    \font\twfvmsy=msym10 \@magscale5
  68.  
  69. %
  70. % Load fonts not normally loaded
  71. %
  72. \font\frtnit=cmti10\@magscale2
  73. \font\svtnit=cmti10\@magscale3
  74. \font\twtyit=cmti10\@magscale4
  75. \font\twfvit=cmti10\@magscale5
  76. \font\twfvsy=cmsy10\@magscale5
  77. \font\twtybf=cmbx10\@magscale4
  78. \font\twfvbf=cmbx10\@magscale5
  79.  
  80. \newfam\msxfam
  81. \newfam\msyfam
  82.  
  83. %
  84. % Now make size changing commands automatically change size of Z symbols
  85. % Doesn't work for letters in the cmex fonts e.g. \bigcup, \sum
  86. %
  87. \def\@vpt{\textfont\msxfam=\fivmsx
  88.     \textfont\msyfam=\fivmsy}
  89. %
  90. \def\@vipt{\textfont\msxfam=\sixmsx
  91.     \textfont\msyfam=\sixmsy}
  92. %
  93. \def\@viipt{\textfont\msxfam=\sevmsx
  94.     \textfont\msyfam=\sevmsy}
  95. %
  96. \def\@viiipt{\textfont\msxfam=\egtmsx
  97.     \textfont\msyfam=\egtmsy}
  98. %
  99. \def\@ixpt{\textfont\msxfam=\ninmsx \scriptfont\msxfam=\sixmsx
  100.     \textfont\msyfam=\ninmsy \scriptfont\msyfam=\sixmsy}
  101. %
  102. \def\@xpt{\textfont\msxfam=\tenmsx \scriptfont\msxfam=\sevmsx
  103.     \textfont\msyfam=\tenmsy \scriptfont\msyfam=\sevmsy}
  104. %
  105. \def\@xipt{\textfont\msxfam=\elvmsx \scriptfont\msxfam=\egtmsx
  106.     \textfont\msyfam=\elvmsy \scriptfont\msyfam=\egtmsy}
  107. %
  108. \def\@xiipt{\textfont\msxfam=\twlmsx \scriptfont\msxfam=\ninmsx
  109.     \textfont\msyfam=\twlmsy \scriptfont\msyfam=\ninmsy}
  110. %
  111. \def\@xivpt{\textfont\msxfam=\frtnmsx \scriptfont\msxfam=\tenmsx
  112.     \textfont\msyfam=\frtnmsy \scriptfont\msyfam=\tenmsy
  113.     \textfont\itfam=\frtnit \scriptfont\itfam=\tenit}
  114. %
  115. \def\@xviipt{\textfont\msxfam=\svtnmsx \scriptfont\msxfam=\twlmsx
  116.     \textfont\msyfam=\svtnmsy \scriptfont\msyfam=\twlmsy
  117.     \textfont\itfam=\svtnit \scriptfont\itfam=\twlit}
  118. %
  119. \def\@xxpt{\textfont\msxfam=\twtymsx \scriptfont\msxfam=\frtnmsx
  120.     \textfont\msyfam=\twtymsy \scriptfont\msyfam=\frtnmsy
  121.     \textfont\bffam=\twtybf
  122.     \textfont\itfam=\twtyit \scriptfont\itfam=\frtnit}
  123. %
  124. \def\@xxvpt{\textfont\msxfam=\twfvmsx \scriptfont\msxfam=\svtnmsx
  125.     \textfont\msyfam=\twfvmsy \scriptfont\msyfam=\svtnmsy
  126.     \textfont\itfam=\twtyit \scriptfont\itfam=\svtnit
  127.     \textfont\bffam=\twfvbf \scriptfont\tw@=\svtnsy}
  128. %
  129.  
  130. \def\bbold{\fam\msyfam}
  131. \def\@famletter#1{\ifcase #1 0\or 1\or 2\or 3\or 4\or 5\or 6\or 7\or
  132.     8\or 9\or A\or B\or C\or D\or E\or F\fi}
  133.  
  134. \edef\@fx{\@famletter\msxfam}
  135. \edef\@fy{\@famletter\msyfam}
  136.  
  137. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  138. %
  139. %    SECTION 2    Z SYMBOLS
  140. %
  141. % The mathcodes for the letters A, ..., Z, a, ..., z are changed to
  142. % generate text italic rather than math italic by default. This makes
  143. % multi-letter identifiers look better. The mathcode for character c
  144. % is set to "7000 (variable family) + "400 (text italic) + c.
  145. %
  146.  
  147. \def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
  148.     \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
  149.     \advance\count0 by1 \advance\count1 by1 \repeat}}
  150.  
  151. \@setmcodes{`A}{`Z}{"7441}
  152. \@setmcodes{`a}{`z}{"7461}
  153. %
  154. % Also, the mathcode for semicolon is set to "8000, so it behaves as an
  155. % active character in math mode; it is defined to insert a thick space.
  156. % \semicolon is a semicolon as an ordinary symbol.
  157. %
  158. \let\@mc=\mathchardef
  159. \mathcode`\;="8000 % Makes ; active in math mode
  160. {\catcode`\;=\active \gdef;{\semicolon\;}}
  161. \@mc\semicolon="603B
  162.  
  163. %
  164. %        ------ UTILITY MACROS FOR Z SYMBOLS ------
  165. %
  166.  
  167. % \z@op        makes a large math operator
  168. % \z@rel    makes a math relation
  169. % \z@bin    makes a binary operator
  170. %
  171. % each use a mathstrut to defeat TeX's vertical adjustment.
  172. % \z@bigXXX big version of symbol
  173. %
  174. \def\z@op#1{\mathop{\mathstrut{#1}}\nolimits}
  175. \def\z@bin#1{\mathbin{\mathstrut{#1}}}
  176. \def\z@rel#1{\mathrel{\mathstrut{#1}}}
  177. %
  178. \def\z@bigop#1{\z@op{\zbig{#1}}}
  179. \def\z@bigbin#1{\z@bin{\zbig{#1}}}
  180. \def\z@bigrel#1{\z@rel{\zbig{#1}}}
  181. %
  182. \def\z@Bigop#1{\z@op{\zBig{#1}}}
  183. \def\z@Bigbin#1{\z@bin{\zBig{#1}}}
  184. \def\z@Bigrel#1{\z@rel{\zBig{#1}}}
  185. %
  186. \def\z@smallop#1{\z@op{\zsmall{#1}}}
  187. \def\z@smallbin#1{\z@bin{\zsmall{#1}}}
  188. \def\z@smallrel#1{\z@rel{\zsmall{#1}}}
  189. %
  190. % This underscore doesn't have the little kern --- you get an italic
  191. % correction anyway in math mode.
  192. \def\_{\leavevmode \vbox{\hrule width0.4em}}
  193.  
  194. % Save \q as \xq for quantifiers q.
  195. \let\xforall=\forall
  196. \let\xexists=\exists
  197. \let\xlambda=\lambda
  198. \let\xmu=\mu
  199. % Save other symbols
  200. \let\xsucc\succ
  201. \let\xprec\prec
  202. \let\dotaccent=\dot
  203. \let\sectionsymbol=\S
  204. \let\integral=\int
  205. \let\product\prod
  206.  
  207. % \p and \f make arrows with 1 and 2 crossings resp.
  208. \def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
  209. \def\f#1{\mathrel{\ooalign{\hfil
  210.     $\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
  211. %
  212. %    ------ AMSTEX SYMBOL DEFINITIONS ------
  213. %
  214. % do these before Z symbols so that we can use them in our special symbols
  215. %
  216. %    msxm font
  217. %
  218. \@mc \boxdot    "2\@fx00
  219. \@mc \boxplus    "2\@fx01
  220. \@mc \boxtimes    "2\@fx02
  221. \@mc \square      "0\@fx03
  222. \@mc \blacksquare    "0\@fx04
  223. \@mc \centerdot    "2\@fx05
  224. \@mc \lozenge    "0\@fx06
  225. \@mc \blacklozenge    "0\@fx07
  226. \@mc \circlearrowright    "3\@fx08
  227. \@mc \circlearrowleft    "3\@fx09
  228. \@mc \rightleftharpoons    "3\@fx0A
  229. \@mc \leftrightharpoons    "3\@fx0B
  230. \@mc \boxminus    "2\@fx0C
  231. \@mc \Vdash    "3\@fx0D
  232. \@mc \Vvdash    "3\@fx0E
  233. \@mc \vDash    "3\@fx0F
  234. \@mc \twoheadrightarrow    "3\@fx10
  235. \@mc \twoheadleftarrow    "3\@fx11
  236. \@mc \leftleftarrows    "3\@fx12
  237. \@mc \rightrightarrows    "3\@fx13
  238. \@mc \upuparrows    "3\@fx14
  239. \@mc \downdownarrows    "3\@fx15
  240. \@mc \upharpoonright    "3\@fx16
  241. \let \restriction    \upharpoonright
  242. \@mc \downharpoonright    "3\@fx17
  243. \@mc \upharpoonleft    "3\@fx18
  244. \@mc \downharpoonleft    "3\@fx19
  245. \@mc \rightarrowtail    "3\@fx1A
  246. \@mc \leftarrowtail    "3\@fx1B
  247. \@mc \leftrightarrows    "3\@fx1C
  248. \@mc \rightleftarrows    "3\@fx1D
  249. \@mc \Lsh    "3\@fx1E
  250. \@mc \Rsh    "3\@fx1F
  251. \@mc \rightsquigarrow    "3\@fx20
  252. \@mc \leftrightsquigarrow    "3\@fx21
  253. \@mc \looparrowleft    "3\@fx22
  254. \@mc \looparrowright    "3\@fx23
  255. \@mc \circeq    "3\@fx24
  256. \@mc \succsim    "3\@fx25
  257. \@mc \gtrsim    "3\@fx26
  258. \@mc \gtrapprox    "3\@fx27
  259. \@mc \multimap    "3\@fx28
  260. \@mc \therefore    "3\@fx29
  261. \@mc \because    "3\@fx2A
  262. \@mc \doteqdot    "3\@fx2B
  263. \let \Doteq    \doteqdot
  264. \@mc \triangleq    "3\@fx2C
  265. \@mc \precsim    "3\@fx2D
  266. \@mc \lesssim    "3\@fx2E
  267. \@mc \lessapprox    "3\@fx2F
  268. \@mc \eqslantless    "3\@fx30
  269. \@mc \eqslantgtr    "3\@fx31
  270. \@mc \curlyeqprec    "3\@fx32
  271. \@mc \curlyeqsucc    "3\@fx33
  272. \@mc \preccurlyeq    "3\@fx34
  273. \@mc \leqq    "3\@fx35
  274. \@mc \leqslant  "3\@fx36
  275. \@mc \lessgtr    "3\@fx37
  276. \@mc \backprime    "0\@fx38
  277. \@mc \risingdotseq    "3\@fx3A
  278. \@mc \fallingdotseq    "3\@fx3B
  279. \@mc \succcurlyeq    "3\@fx3C
  280. \@mc \geqq    "3\@fx3D
  281. \@mc \geqslant  "3\@fx3E
  282. \@mc \gtrless    "3\@fx3F
  283. \@mc \sqsubset    "3\@fx40
  284. \@mc \sqsupset    "3\@fx41
  285. \@mc \vartriangleright    "3\@fx42
  286. \@mc \vartriangleleft    "3\@fx43
  287. \@mc \trianglerighteq    "3\@fx44
  288. \@mc \trianglelefteq    "3\@fx45
  289. \@mc \bigstar    "0\@fx46
  290. \@mc \between    "3\@fx47
  291. \@mc \blacktriangledown    "0\@fx48
  292. \@mc \blacktriangleright    "3\@fx49
  293. \@mc \blacktriangleleft    "3\@fx4A
  294. \@mc \vartriangle    "0\@fx4D
  295. \@mc \blacktriangle    "0\@fx4E
  296. \@mc \triangledown    "0\@fx4F
  297. \@mc \eqcirc    "3\@fx50
  298. \@mc \lesseqgtr    "3\@fx51
  299. \@mc \gtreqless    "3\@fx52
  300. \@mc \lesseqqgtr    "3\@fx53
  301. \@mc \gtreqqless    "3\@fx54
  302. \def \yen    {\mathhexbox\@fx55 }
  303. \@mc \Rrightarrow    "3\@fx56
  304. \@mc \Lleftarrow    "3\@fx57
  305. \def \checkmark    {\mathhexbox\@fx58 }
  306. \@mc \veebar    "2\@fx59
  307. \@mc \barwedge    "2\@fx5A
  308. \@mc \doublebarwedge    "2\@fx5B
  309. \@mc \angle    "0\@fx5C
  310. \@mc \measuredangle    "0\@fx5D
  311. \@mc \sphericalangle    "0\@fx5E
  312. \@mc \varpropto    "3\@fx5F
  313. \@mc \smallsmile    "3\@fx60
  314. \@mc \smallfrown    "3\@fx61
  315. \@mc \Subset    "3\@fx62
  316. \@mc \Supset    "3\@fx63
  317. \@mc \Cup    "2\@fx64
  318. \let \doublecup    \Cup
  319. \@mc \Cap    "2\@fx65
  320. \let \doublecap    \Cap
  321. \@mc \curlywedge    "2\@fx66
  322. \@mc \curlyvee    "2\@fx67
  323. \@mc \leftthreetimes    "2\@fx68
  324. \@mc \rightthreetimes    "2\@fx69
  325. \@mc \subseteqq    "3\@fx6A
  326. \@mc \supseteqq    "3\@fx6B
  327. \@mc \bumpeq    "3\@fx6C
  328. \@mc \Bumpeq    "3\@fx6D
  329. \@mc \lll    "3\@fx6E
  330. \let \llless    \lll
  331. \@mc \ggg    "3\@fx6F
  332. \let \gggtr    \ggg
  333. \def \ulcorner    {\delimiter"4\@fx70\@fx70 }
  334. \def \urcorner    {\delimiter"5\@fx71\@fx71 }
  335. \def \circledR    {\mathhexbox\@fx72 }
  336. \@mc \circledS    "0\@fx73
  337. \@mc \pitchfork    "3\@fx74
  338. \@mc \dotplus    "2\@fx75
  339. \@mc \backsim    "3\@fx76
  340. \@mc \backsimeq    "3\@fx77
  341. \def \llcorner    {\delimiter"4\@fx78\@fx78 }
  342. \def \lrcorner    {\delimiter"5\@fx79\@fx79 }
  343. \def \maltese    {\mathhexbox\@fx7A }
  344. \@mc \complement    "0\@fx7B
  345. \@mc \intercal    "2\@fx7C
  346. \@mc \circledcirc    "2\@fx7D
  347. \@mc \circledast    "2\@fx7E
  348. \@mc \circleddash    "2\@fx7F
  349. %
  350. %    msym font
  351. %
  352. \@mc \lvertneqq "3\@fy00
  353. \@mc \gvertneqq "3\@fy01
  354. \@mc \nleq    "3\@fy02
  355. \@mc \ngeq    "3\@fy03
  356. \@mc \nless    "3\@fy04
  357. \@mc \ngtr    "3\@fy05
  358. \@mc \nprec    "3\@fy06
  359. \@mc \nsucc    "3\@fy07
  360. \@mc \lneqq    "3\@fy08
  361. \@mc \gneqq    "3\@fy09
  362. \@mc \nleqslant    "3\@fy0A
  363. \@mc \ngeqslant    "3\@fy0B
  364. \@mc \lneq    "3\@fy0C
  365. \@mc \gneq    "3\@fy0D
  366. \@mc \npreceq    "3\@fy0E
  367. \@mc \nsucceq    "3\@fy0F
  368. \@mc \precnsim    "3\@fy10
  369. \@mc \succnsim    "3\@fy11
  370. \@mc \lnsim    "3\@fy12
  371. \@mc \gnsim    "3\@fy13
  372. \@mc \nleqq    "3\@fy14
  373. \@mc \ngeqq    "3\@fy15
  374. \@mc \precneqq    "3\@fy16
  375. \@mc \succneqq    "3\@fy17
  376. \@mc \precnapprox    "3\@fy18
  377. \@mc \succnapprox    "3\@fy19
  378. \@mc \lnapprox    "3\@fy1A
  379. \@mc \gnapprox    "3\@fy1B
  380. \@mc \nsim    "3\@fy1C
  381. \@mc \ncong    "3\@fy1D
  382. \def \napprox    {\not\approx}
  383. %\@mc \varsubsetneq "3\@fy20
  384. %\@mc \varsupsetneq "3\@fy21
  385. \@mc \nsubseteqq    "3\@fy22
  386. \@mc \nsupseteqq    "3\@fy23
  387. \@mc \subsetneqq    "3\@fy24
  388. \@mc \supsetneqq    "3\@fy25
  389. %\@mc \varsubsetneqq    "3\@fy26
  390. %\@mc \varsupsetneqq    "3\@fy27
  391. \@mc \subsetneq    "3\@fy28
  392. \@mc \supsetneq    "3\@fy29
  393. \@mc \nsubseteq    "3\@fy2A
  394. \@mc \nsupseteq    "3\@fy2B
  395. \@mc \nparallel    "3\@fy2C
  396. \@mc \nmid    "3\@fy2D
  397. \@mc \nshortmid    "3\@fy2E
  398. \@mc \nshortparallel    "3\@fy2F
  399. \@mc \nvdash    "3\@fy30
  400. \@mc \nVdash    "3\@fy31
  401. \@mc \nvDash    "3\@fy32
  402. \@mc \nVDash    "3\@fy33
  403. \@mc \ntrianglerighteq    "3\@fy34
  404. \@mc \ntrianglelefteq    "3\@fy35
  405. \@mc \ntriangleleft    "3\@fy36
  406. \@mc \ntriangleright    "3\@fy37
  407. \@mc \nleftarrow    "3\@fy38
  408. \@mc \nrightarrow    "3\@fy39
  409. \@mc \nLeftarrow    "3\@fy3A
  410. \@mc \nRightarrow    "3\@fy3B
  411. \@mc \nLeftrightarrow    "3\@fy3C
  412. \@mc \nleftrightarrow    "3\@fy3D
  413. \@mc \divideontimes    "2\@fy3E
  414. \@mc \varnothing    "0\@fy3F
  415. \@mc \mho    "0\@fy66
  416. \@mc \eth    "0\@fy67
  417. \@mc \eqsim    "3\@fy68
  418. \@mc \beth    "0\@fy69
  419. \@mc \gimel    "0\@fy6A
  420. \@mc \daleth    "0\@fy6B
  421. \@mc \lessdot    "3\@fy6C
  422. \@mc \gtrdot    "3\@fy6D
  423. \@mc \ltimes    "2\@fy6E
  424. \@mc \rtimes    "2\@fy6F
  425. \@mc \shortmid    "3\@fy70
  426. \@mc \shortparallel    "3\@fy71
  427. \def \interleave    {{\parallel\!\!\vert}}
  428. \def \shortinterleave    {\z@rel{\mathord\shortmid\mathord\shortparallel}}
  429. \@mc \smallsetminus    "2\@fy72
  430. \@mc \thicksim    "3\@fy73
  431. \@mc \thickapprox    "3\@fy74
  432. \@mc \approxeq    "3\@fy75
  433. \@mc \succapprox    "3\@fy76
  434. \@mc \precapprox    "3\@fy77
  435. \@mc \curvearrowleft    "3\@fy78
  436. \@mc \curvearrowright    "3\@fy79
  437. \@mc \digamma    "0\@fy7A
  438. \@mc \varkappa    "0\@fy7B
  439. \@mc \hslash    "0\@fy7D
  440. \@mc \hbar    "0\@fy7E
  441. \@mc \backepsilon    "3\@fy7F
  442. %
  443. %        ------ SPECIAL Z SYMBOLS ------
  444. %
  445. %    NUMBERS
  446. %
  447. \def \nat    {{\bbold N}}
  448. \def \integer    {{\bbold Z}}
  449. \def \natone    {{\bbold N}_1}
  450. \def \real    {{\bbold R}}
  451. \def \bool    {{\bbold B}}
  452. \let \divides    \div
  453. \def \div    {\z@bin{\rm div}}
  454. \def \mod    {\z@bin{\rm mod}}
  455. \def \succ    {\word{succ}}
  456. \def \expon    {^}
  457. %    aliases
  458. \let \num    \integer
  459. \let \nplus    \natone
  460. %
  461. %    LOGIC
  462. %
  463. \def \lnot    {\neg\;}
  464. \def \land    {\z@rel{\wedge}}
  465. \def \lor    {\z@rel{\vee}}
  466. \let \imp    \Rightarrow
  467. \let \iff    \Leftrightarrow
  468. \def \all    {\z@op{\xforall}}
  469. \def \exi    {\z@op{\xexists}}
  470. \def \exione    {\exists_1}
  471. \@mc \nexi    "0\@fy40
  472. \def \dot    {\z@rel{\bullet}}
  473. \def \true    {\keyword{true}}
  474. \def \false    {\keyword{false}}
  475. \let \cond    \rightarrow
  476. %    aliases
  477. \let \spot    \dot
  478. \mathcode`\@="8000% make @ active in mathmode
  479. {\catcode`\@=\active \gdef@{\dot}}
  480. \let \implies    \imp
  481. \let \forall    \all
  482. \let \exists    \exi
  483. \let \nexists    \nexi
  484. %
  485. %    SETS
  486. %
  487. \let \emptyset  \varnothing
  488. \def \varemptyset  {\{\,\}}
  489. \def \pset    {\z@op{\bbold P}}
  490. \def \psetone    {\pset_1}
  491. \def \fset    {\z@op{\bbold F}}
  492. \def \fsetone    {\fset_1}
  493. \def \sset    {\z@op{\bbold S}}
  494. \let \mem    \in
  495. \def \nem    {\not\mem}
  496. \def \uni    {\z@bin\cup}
  497. \def \int    {\z@bin\cap}
  498. \let \prod    \times
  499. \def \min    {\word{min}}
  500. \def \max    {\word{max}}
  501. \def \duni    {\z@Bigop{\lower0.25ex\hbox{$\uni$}}}
  502. \def \dint    {\z@Bigop{\lower0.25ex\hbox{$\int$}}}
  503. \def \upto    {\z@bin{\ldotp\ldotp}}
  504. \let \psubs    \subset
  505. \let \subs    \subseteq
  506. \let \psups    \supset
  507. \let \sups    \supseteq
  508. \def \diff    {\z@bin{\backslash}}
  509. %    aliases
  510. \let \cross    \prod
  511. \let \notin    \nem
  512. \let \nmem    \nem
  513. \let \union    \uni
  514. \let \inter    \int
  515. \let \power    \pset
  516. \let \finset    \fset
  517. \let \dunion    \duni
  518. \let \dinter    \dint
  519. %
  520. %    RELATIONS & FUNCTIONS
  521. %
  522. \def \lambda    {\z@op{\xlambda}}
  523. \def \mu    {\z@op{\xmu}}
  524. \def \dom    {\keyword{dom}}
  525. \def \ran    {\keyword{ran}}
  526. \def \id    {\keyword{id}}
  527. \@mc \dres    "2\@fx43
  528. \@mc \rres    "2\@fx42
  529. \def \dsub    {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\dres}}}
  530. \def \rsub    {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\rres}}}
  531. \let \fovr    \oplus
  532. \let \cmp    \circ
  533. \def \fcmp    {\mathbin{\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle
  534.          \rm o$\hfil\cr\hfil$\scriptscriptstyle\rm 9$\hfil}}}}
  535. \def \inv    {^{-1}}
  536. \def \limg    {(\!|}
  537. \def \rimg    {|\!)}
  538. \let \map    \mapsto
  539. \let \rel    \leftrightarrow
  540. \let \tfun    \rightarrow
  541. \let \tinj    \rightarrowtail
  542. \def \tsur    {\mathrel{\ooalign{$\tfun$\hfil\cr$\mkern4mu\tfun$}}}
  543. \def \pfun    {\p\tfun}
  544. \def \pinj    {\p\tinj}
  545. \def \psur    {\p\tsur}
  546. \def \ffun    {\f\tfun}
  547. \def \finj    {\f\tinj}
  548. \def \bij    {\mathrel{\ooalign{$\tinj$\hfil\cr$\mkern5mu\tfun$}}}
  549. \def \tcl    {^+}
  550. \def \rtcl    {^*}
  551. \def \iter    {^}
  552. %    aliases
  553. \let \comp    \fcmp
  554. \let \ndres    \dsub
  555. \let \nrres    \rsub
  556. \let \fun    \tfun
  557. \let \inj    \tinj
  558. \let \surj    \tsur
  559. \let \psurj    \psur
  560. %
  561. %    SEQUENCES
  562. %
  563. \def \seq    {\keyword{seq}}
  564. \def \seqone    {\seq_1}
  565. \def \emptyseq  {\lseq\,\rseq}
  566. \let \lseq    \langle
  567. \let \rseq    \rangle
  568. \def \head    {\word{head}}
  569. \def \tail    {\word{tail}}
  570. \def \front    {\word{front}}
  571. \def \last    {\word{last}}
  572. \def \rev    {\word{rev}}
  573. \def \squash    {\word{squash}}
  574. \def \next    {\keyword{next}}
  575. \def \inseq    {\keyword{in}}
  576. \def \cat    {\mathbin{\raise 0.8ex\hbox{$\mathchar"2\@fx61$}}}
  577. \@mc \sres    "2\@fx16
  578. \def \ssub    {\z@bin{\rlap{$-$}{\sres}}}
  579. \@mc \ires    "2\@fx18
  580. \def \isub    {\z@bin{\rlap{$-$}{\ires}}}
  581. \def \dcat    {\z@op{\cat/}}
  582. \def \dovr    {\z@op{\fovr/}}
  583. \def \dcmp    {\z@op{\fcmp/}}
  584. \let \prefix    \subseteq
  585. \def \suffix    {\keyword{suffix}}
  586. \def \seqi    {\keyword{seq_\infty}}
  587. \def \partitions    {\keyword{partitions}}
  588. \def \disjoint    {\keyword{disjoint}}
  589. \def \subseq    {\keyword{subseq}}
  590. %    aliases
  591. \let \filter    \sres
  592. %
  593. %    SCHEMAS
  594. %
  595. \def \lsch    {\z@bigop{\hbox{[}}}
  596. \def \rsch    {\z@bigop{\hbox{]}}}
  597. \def \dparallel    {\z@bigop{\parallel}\limits}
  598. \def \zand    {\z@bigbin\land}
  599. \def \zor    {\z@bigbin\lor}
  600. \def \zcmp    {\z@bigbin\fcmp}
  601. \def \zexi    {\z@bigop\exists}
  602. \def \zall    {\z@bigop\forall}
  603. \def \znot    {\z@bigop\neg}
  604. \def \zbar    {\z@bigbin\cbar}
  605. \def \zfor    {/}
  606. \def \zhide    {\z@bigbin\backslash}
  607. \def \zimp    {\z@bigrel\imp}
  608. \def \zeq    {\z@bigrel\iff}
  609. \def \zovr    {\z@bigrel\oplus}
  610. \def \zpipe    {\z@bigbin{\mathord>\!\!\mathord>}}
  611. \def \pre    {\keyword{pre}}
  612. \def \pred    {\keyword{pred}}
  613. \def \post    {\keyword{post}}
  614. \def \zproject    {\z@bigbin\sres}
  615. \def\rename{\@ifnextchar*{\z@rename}{\z@@rename}}
  616. \def\z@rename*[#1/#2]{\left[#1 \over #2\right]}
  617. \def\z@@rename[#1/#2]{\left[#1 \zfor #2\right]}
  618. %    aliases
  619. \let \project    \zproject
  620. \let \import    \sres
  621. \let \semi    \zcmp
  622. \let \hide    \zhide
  623. %
  624. %    BAGS
  625. %
  626. \let\buni\uplus
  627. \def \emptybag  {\lbag\:\rbag}
  628. \def \lbag    {[\![}
  629. \def \rbag    {]\!]}
  630. \def \bag    {\keyword{bag}}
  631. \def \items    {\word{items}}
  632. \let \inbag    \inseq
  633. \def \bagcount    {\word{count}}
  634. %
  635. %    DEFINITIONS & DECLARATIONS
  636. %
  637. \def \ddef    {\z@rel{\;::=\;}}
  638. \def \bbar    {\z@bigrel\mid}
  639. \let \cbar    \mid
  640. \def \lang    {\langle\!\langle}
  641. \def \rang    {\rangle\!\rangle}
  642. \def \sdef    {\z@rel{\widehat=}}
  643. \def \defs    {\z@smallrel{==}}
  644. \def \varsdef    {\z@rel\triangleq}
  645. %    aliases
  646. \let \sdefs    \sdef
  647. \mathcode`\|=\mid
  648. \let \ldata    \lang
  649. \let \rdata    \rang
  650. %
  651. %    MISCELLANEOUS
  652. %
  653. \def \lblot     {\langle\!|}
  654. \def \rblot     {|\!\rangle}
  655. \def \IMP    {\boldword{Import}}
  656. \let \env    \Rrightarrow
  657. \def \zlet      {\boldword{let}}
  658. \def \zin       {\boldword{in}}
  659. \def \zwhere    {\boldword{where}}
  660. %
  661. %    QZED SUPPORT
  662. %
  663. \def\HOLE{\z@op{\hbox{$\lll\star\star\star\ggg$}}}
  664. \def\landd{} % to support qzed editor
  665. \def\semid{} % to support qzed editor
  666. \def\qzed{\ifz@inclass\else\zed\fi}
  667. \def\endqzed{\ifz@inclass\else\endzed\fi}
  668. %
  669. %    CLASSES
  670. %
  671. \def\qua{\mbox{::}}
  672. \def\redef{\mbox{\bf ~redef}}
  673. \def\Init{I\!{\scriptstyle NIT}}
  674. \def\Exit{E\!{\scriptstyle XIT}}
  675. \def\Internal{I\!{\scriptstyle NTERNAL}}
  676. \def\Aux{A\!{\scriptstyle UX}}
  677. \def\intern{\mbox{\sf i}}
  678. %
  679. %        ------ OTHER SPECIAL NOTATION ------
  680. %
  681. %    PROOFS
  682. %
  683. \def\thrm{\z@rel\vdash}
  684. \def\qed{\zsmall\Box}
  685. \let\Qed\Box
  686. \let\QED\square
  687. \def\BLACKQED{\zsmall\blacksquare}
  688. \let\ETH\qed
  689. \def\TH{\boldword{Theorem}}
  690. \def\LE{\boldword{Lemma}}
  691. \def\PR{\boldword{Proof}}
  692. \def\refines{\z@rel\sqsupseteq}
  693. \def\defines{\z@rel\sqsubseteq}
  694. \def\weakrefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsupset$}}\lower1ex\hbox{$\sim$}}}
  695. \def\weakdefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsubset$}}\lower1ex\hbox{$\sim$}}}
  696. %    aliases
  697. \let\shows\thrm
  698. %
  699. %    OBJECT THEORY
  700. %
  701. \def\childof{\z@rel\xsucc}
  702. \def\parentof{\z@rel\xprec}
  703. \let\weaksubclass\succsim
  704. \let\weaksupclass\precsim
  705. \def\hasa{\z@rel{\mathord\xsucc\!\!\!\mathord\xsucc}}
  706. \def\instancein{\z@rel{\mathord\xprec\!\!\!\mathord\xprec}}
  707. \def\subtype{\z@rel\sqsubset}
  708. \def\subtypeeq{\z@rel\sqsubseteq}
  709. \def\suptype{\z@rel\sqsupset}
  710. \def\suptypeeq{\z@rel\sqsupseteq}
  711. %    aliases
  712. \let\inherits\childof
  713. \let\subclass\childof
  714. \let\isa\childof
  715. \let\supclass\parentof
  716. \let\instantiates\hasa
  717. \let\islikea\weaksubclass
  718. %
  719. %    TEMPORAL LOGIC
  720. %
  721. \def\atnext{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\zSmall\bigcirc}
  722. \def\atlast{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\kern0.01em\mathord-$}\zSmall\bigcirc}
  723. \def\always{\lower0.37ex\hbox{$\zbig\Box$}}
  724. \def\uptilnow{\rlap{$\kern0.02em\mathord-$}\lower0.37ex\hbox{$\zbig\Box$}}
  725. \def\eventually{\lower0.37ex\hbox{$\zbig\Diamond$}}
  726. \def\previously{\rlap{$\kern0.04em\mathord-$}\lower0.37ex\hbox{$\zbig\Diamond$}}
  727. %    aliases
  728. \let\henceforth\always
  729. %
  730. %    ORDERS
  731. %
  732. \def \mono    {\keyword{monotonic}}
  733. \def \porder    {\keyword{partial\_order}}
  734. \def \torder    {\keyword{total\_order}}
  735. %
  736. %    WORD STYLES
  737. %
  738. \def\String#1{\hbox{`{\tt #1}'}}
  739. \def\STRING#1{\hbox{``{\tt #1}''}}
  740. \def\infix#1{\z@rel{{\underline{#1}}}}
  741. \def\word#1{\z@op{#1}}
  742. \def\keyword#1{\z@op{\rm #1}}
  743. \def\boldword#1{\z@op{\bf #1}}
  744. \def\underword#1{\z@op{{\underline{#1}}}}
  745. \def\underkeyword#1{\z@op{{\underline{\rm #1}}}}
  746. \def\underboldword#1{\z@op{{\underline{\bf #1}}}}
  747. \newbox\z@combox\newdimen\z@wdcalc
  748. \def\comment{\@ifnextchar*{\z@leftcomment}{\z@comment}}
  749. \def\z@comment#1{$\z@stopfield\z@addfield\z@startfield$\global\setbox\z@combox\hbox{\quad[{\sf #1}]}\z@wdcalc=\wd\z@combox\advance\z@wdcalc by \wd\z@curline\advance\z@wdcalc by \z@curindent\advance\z@wdcalc by \zedleftsep\advance\z@wdcalc by \zedlinethickness\advance\z@wdcalc by 2\zedindent\ifdim\z@wdcalc>\displaywidth\\\fi&\box\z@combox\ignorespaces}
  750. \def\z@leftcomment*#1{\hbox{[{\sf #1}]}}
  751. %
  752. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  753. %
  754. %    SECTION 3    Z ENVIRONMENTS
  755. %
  756. %        ------ MARGIN STACK ------
  757. %
  758. % define a stack of dimensions (50 elements)
  759. %    can probably be made smaller when qzed filters its TeX output better
  760. \newcount\z@stackmin
  761. \newcount\z@stackmax
  762. \newcount\z@stacktop
  763. \newdimen\@gtempa \z@stackmin=\allocationnumber
  764. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  765. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  766. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  767. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  768. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  769. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  770. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  771. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  772. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  773. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  774. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  775. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  776. \newdimen\@getempa \z@stackmax=\allocationnumber
  777. \dimen\z@stackmin=0pt
  778.  
  779. % define a box to contain the current line
  780. %  & a variable to contain it's indentation
  781. \newbox\z@curline
  782. \newdimen\z@curindent
  783. \dimen\z@curindent=0pt
  784. % Space between operands of a function application
  785. \def\z@space{{}\;{}}
  786.  
  787. % define a box to contain the current field
  788. \newbox\z@curfield
  789.  
  790. % define a mini-tabbing environment for use inside 'zed'
  791. \def\z@startline{\setbox\z@curline\hbox{}%
  792.                  \global\z@curindent\dimen\z@stacktop
  793.                  \z@startfield\ignorespaces}
  794. \def\z@stopline{\z@stopfield
  795.                 \z@addfield
  796.                 \hbox{\hskip\z@curindent \box\z@curline}}
  797.  
  798. \def\z@startfield{\global\setbox\z@curfield\hbox\bgroup}
  799. \def\z@stopfield{\egroup}
  800. \def\z@addfield{\global\setbox\z@curline\hbox{\unhbox
  801.                  \z@curline\unhbox\z@curfield}}
  802.  
  803. \def\z@pushmargin{\hbox{\kern0pt}$%
  804.                   \z@stopfield
  805.                   \z@addfield
  806.                   \ifnum \z@stacktop < \z@stackmax
  807.                     \global\advance\z@stacktop \@ne
  808.                   \else
  809.                     \@latexerr{Z margin stack overflow (too many \string\M's)}
  810.             \@ehd
  811.                   \fi
  812.                   \global\dimen\z@stacktop\z@curindent
  813.                   \global\advance\dimen\z@stacktop \wd\z@curline
  814.                   \z@startfield\ignorespaces
  815.                   $\relax}
  816. \def\z@popmargin{\ifnum \z@stacktop > \z@stackmin
  817.                     \global\advance\z@stacktop \m@ne \ignorespaces
  818.                   \else
  819.                     \@latexerr{Z Margin stack underflow (too many \string\O's)}
  820.             \@ehd
  821.                   \fi}
  822. \def\M{\z@pushmargin} \def\O{\z@popmargin} \def\S{\z@space}
  823. \z@stacktop\z@stackmin
  824. %
  825. %        ------ UTILITY MACROS FOR Z ENVIRONMENTS ------
  826. %
  827. % Here are environments for the various sorts of displays which occur in
  828. % Z documents. All displays are set flush left, indented by \zedindent,
  829. % by default \leftmargini.  Schemas, etc, are made just wide enough to
  830. % give equal margins left and right.
  831. %
  832. % Some environments (schema, etc.) must only be split at `\zbreak',
  833. % and others (e.g. argue) may be split arbitrarily. All generate
  834. % alignment displays, and penalties are used to control page breaks.
  835. %
  836. %    FORMAT and CONTROL macros
  837. %
  838. \newdimen\zedindent        \zedindent=\leftmargini
  839. \newdimen\zedleftsep        \zedleftsep=1em
  840. \newdimen\zedtab        \zedtab=2em
  841. \newdimen\zedbar        \zedbar=8em
  842. \newdimen\zedlinethickness    \zedlinethickness=0.4pt
  843. \newdimen\zedcornerheight    \zedcornerheight=0pt
  844. \newcount\z@cols
  845. %
  846. \newif\ifz@firstline        \z@firstlinefalse
  847. \newif\ifz@inclass        \z@inclassfalse
  848. \newif\ifz@inenv        \z@inenvfalse
  849. \newif\ifz@leftmargin        \z@leftmargintrue
  850. \newif\ifz@incols        \z@incolsfalse
  851. \newif\ifleftnames        \leftnamesfalse
  852. \def\leftschemas{\leftnamestrue}
  853. \newif\ifz@inbox        \z@inboxfalse
  854. %
  855. \newskip\zedbaselineskip    \zedbaselineskip\baselineskip
  856. \newbox\zstrutbox        \setbox\zstrutbox=\copy\strutbox
  857. \def\zstrut{\relax\ifmmode\copy\zstrutbox\else\unhcopy\zstrutbox\fi}
  858. \def\zedbaselinestretch{1}
  859. %
  860. % penalties
  861. %
  862. \newcount\interzedlinepenalty    \interzedlinepenalty=10000    %never break
  863. \newcount\preboxpenalty        \preboxpenalty=0        %break easily
  864. \newcount\forcepagepenalty    \forcepagepenalty=-10000    %always break
  865. % also use            \interdisplaylinepenalty=100    %break sometimes
  866. %
  867. % macros for changing the size of schema text
  868. %
  869. \def\zedsize#1{\def\z@size{#1}}
  870. \def\z@size{}
  871. \newskip\z@adskip\newskip\z@bdskip\newskip\z@adsskip\newskip\z@bdsskip
  872. \def\z@changesize{%
  873. \z@adskip\abovedisplayskip\z@bdskip\belowdisplayskip% save skips
  874. \z@adsskip\abovedisplayshortskip\z@bdsskip\belowdisplayshortskip
  875. \z@size % change size
  876. \abovedisplayskip\z@adskip\belowdisplayskip\z@bdskip% restore skips
  877. \abovedisplayshortskip\z@adsskip\belowdisplayshortskip\z@bdsskip}
  878. %
  879. \def\zBIG#1{\hbox{\ifx\z@ptsize \vpt \viiipt\@viiipt
  880.     \else \ifx\z@ptsize \vipt \ixpt\@ixpt
  881.     \else \ifx\z@ptsize \viipt \xpt\@xpt
  882.     \else \ifx\z@ptsize \viiipt \xipt\@xipt
  883.     \else \ifx\z@ptsize \ixpt \xiipt\@xiipt
  884.     \else \ifx\z@ptsize \xpt \xivpt\@xivpt
  885.     \else \ifx\z@ptsize \xipt \xviipt\@xviipt
  886.     \else \ifx\z@ptsize \xiipt \xxpt\@xxpt
  887.     \else \ifx\z@ptsize \xivpt \xxvpt\@xxvpt
  888.     \else \ifx\z@ptsize \xviipt \xxvpt\@xxvpt
  889.     \else \ifx\z@ptsize \xxpt \xxvpt\@xxvpt
  890.     \else \@warning{Can't increase this font size}
  891.     \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
  892. \def\zBig#1{\hbox{\ifx\z@ptsize \vpt \viipt\@viipt
  893.     \else \ifx\z@ptsize \vipt \viiipt\@viiipt
  894.     \else \ifx\z@ptsize \viipt \ixpt\@ixpt
  895.     \else \ifx\z@ptsize \viiipt \xpt\@xpt
  896.     \else \ifx\z@ptsize \ixpt \xipt\@xipt
  897.     \else \ifx\z@ptsize \xpt \xiipt\@xiipt
  898.     \else \ifx\z@ptsize \xipt \xivpt\@xivpt
  899.     \else \ifx\z@ptsize \xiipt \xviipt\@xviipt
  900.     \else \ifx\z@ptsize \xivpt \xxpt\@xxpt
  901.     \else \ifx\z@ptsize \xviipt \xxvpt\@xxvpt
  902.     \else \ifx\z@ptsize \xxpt \xxvpt\@xxvpt
  903.     \else \@warning{Can't increase this font size}
  904.     \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
  905. \def\zbig#1{\hbox{\ifx\z@ptsize \vpt \vipt\@vipt
  906.     \else \ifx\z@ptsize \vipt \viipt\@viipt
  907.     \else \ifx\z@ptsize \viipt \viiipt\@viiipt
  908.     \else \ifx\z@ptsize \viiipt \ixpt\@ixpt
  909.     \else \ifx\z@ptsize \ixpt \xpt\@xpt
  910.     \else \ifx\z@ptsize \xpt \xipt\@xipt
  911.     \else \ifx\z@ptsize \xipt \xiipt\@xiipt
  912.     \else \ifx\z@ptsize \xiipt \xivpt\@xivpt
  913.     \else \ifx\z@ptsize \xivpt \xviipt\@xviipt
  914.     \else \ifx\z@ptsize \xviipt \xxpt\@xxpt
  915.     \else \ifx\z@ptsize \xxpt \xxvpt\@xxvpt
  916.     \else \@warning{Can't increase this font size}
  917.     \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
  918. \def\zsmall#1{\hbox{\ifx\z@ptsize \vipt \vpt\@vpt
  919.     \else \ifx\z@ptsize \viipt \vipt\@vipt
  920.     \else \ifx\z@ptsize \viiipt \viipt\@viipt
  921.     \else \ifx\z@ptsize \ixpt \viiipt\@viiipt
  922.     \else \ifx\z@ptsize \xpt \ixpt\@ixpt
  923.     \else \ifx\z@ptsize \xipt \xpt\@xpt
  924.     \else \ifx\z@ptsize \xiipt \xipt\@xipt
  925.     \else \ifx\z@ptsize \xivpt \xiipt\@xiipt
  926.     \else \ifx\z@ptsize \xviipt \xivpt\@xivpt
  927.     \else \ifx\z@ptsize \xxpt \xviipt\@xviipt
  928.     \else \ifx\z@ptsize \xxvpt \xxpt\@xxpt
  929.     \else \@warning{Can't decrease this font size}
  930.     \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
  931. \def\zSmall#1{\hbox{\ifx\z@ptsize \vipt \vpt\@vpt
  932.     \else \ifx\z@ptsize \viipt \vpt\@vpt
  933.     \else \ifx\z@ptsize \viiipt \vipt\@vipt
  934.     \else \ifx\z@ptsize \ixpt \viipt\@viipt
  935.     \else \ifx\z@ptsize \xpt \viiipt\@viiipt
  936.     \else \ifx\z@ptsize \xipt \ixpt\@ixpt
  937.     \else \ifx\z@ptsize \xiipt \xpt\@xpt
  938.     \else \ifx\z@ptsize \xivpt \xipt\@xipt
  939.     \else \ifx\z@ptsize \xviipt \xiipt\@xiipt
  940.     \else \ifx\z@ptsize \xxpt \xivpt\@xivpt
  941.     \else \ifx\z@ptsize \xxvpt \xviipt\@xviipt
  942.     \else \@warning{Can't decrease this font size}
  943.     \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
  944. %
  945. \def\z@zeroskips{\abovedisplayskip\z@\belowdisplayskip\z@
  946.     \abovedisplayshortskip\z@\belowdisplayshortskip\z@}
  947. %
  948. %    Make zedbaselinestretch have an automatic effect
  949. %        adapted from lfonts.tex
  950. %
  951. \def\@setsize#1#2#3#4{\@nomath#1\let\@currsize#1\baselineskip
  952.     #2\baselineskip\baselinestretch\baselineskip
  953.     \setbox\strutbox\hbox{\vrule height.7\baselineskip
  954.     depth.3\baselineskip width\z@}\normalbaselineskip
  955.     \baselineskip #3#4\zedbaselineskip
  956.     #2\zedbaselineskip\zedbaselinestretch\zedbaselineskip
  957.     \setbox\zstrutbox\hbox{\vrule height.7\zedbaselineskip
  958.     depth.3\zedbaselineskip width\z@}\let\z@ptsize#3}
  959. %
  960. %        ------ MACROS FOR MARGINS ------
  961. %
  962. % \z@narrow, \z@wide - make the margins narrower, wider
  963. %
  964. \def\z@narrow{\advance\linewidth by -\zedindent}
  965. \def\z@wide{\advance\linewidth by \zedindent}
  966. %
  967. %        ------ MACROS FOR DRAWING BOXES ------
  968. %
  969. % \z@hrulefill - line with correct thickness
  970. %
  971. \def\z@hrulefill{\leaders\hrule height\zedlinethickness\hfill}
  972. %
  973. % \z@topline draws the top horizontal line of boxed environments
  974. % \z@dbltopline draws a double ruled top line
  975. % \z@botline draws the bottom horizontal line of boxed environments
  976. % \zedline[comment] draws a long horizontal line ending in comment
  977. % \where draws a short horizontal line
  978. %
  979. \def\z@topline#1{\omit\@ifnextchar[{\z@@topline{#1}}{\z@@topline{#1}[]}}
  980. \def\z@@topline#1[#2]{\hbox to\linewidth{\zstrut\ifleftnames\else
  981.     \vrule height\zedlinethickness width\zedlinethickness
  982.     \hbox to\zedleftsep{\z@hrulefill}\fi#1\z@hrulefill
  983.     \smash{\vrule height\zedlinethickness width\zedlinethickness
  984.     depth\zedcornerheight}\hbox{\sf #2}}\cr}
  985. \def\z@dbltopline#1{\omit\@ifnextchar[{\z@@dbltopline{#1}}{\z@@dbltopline{#1}[]}}
  986. \def\z@@dbltopline#1[#2]{\z@@topline{#1}[#2]%
  987. \noalign{\kern-\baselineskip
  988.     \kern-\zedlinethickness
  989.     \kern-\doublerulesep \nobreak}%
  990. \omit\z@@topline{\hphantom{#1}}[\hphantom{#2}]%
  991. \noalign{\kern\doublerulesep
  992.     \kern\zedlinethickness \nobreak}}
  993. \def\z@botline{\also\omit\hbox to\linewidth{\z@hrulefill
  994. \smash{\vrule height\zedcornerheight width\zedlinethickness
  995.         depth 0pt}}\cr}
  996. \def\z@@botline[#1]{\hbox to\linewidth{\vrule\z@hrulefill\hbox{\sf\smash{#1}}}\also}
  997. \def\zedline{\also\omit\@ifnextchar[{\z@@botline}{\z@@botline[]}}
  998. \def\where{\also \omit \hbox to\zedbar{\z@hrulefill}\cr\also}
  999. \let \ST    \where
  1000. %
  1001. % \z@left is placed at the left of each z line:
  1002. %    in non-box environments it will do nothing.
  1003. %    in boxed environments it will do a vertical line with the same
  1004. %        height as the maximum height of the line.
  1005. %
  1006. \def\z@left{\ifz@inbox\vrule width\zedlinethickness\hskip\zedleftsep\fi}
  1007. %
  1008. %        ------ MACROS FOR SETTING UP Z ENVIRONMENTS ------
  1009. %
  1010. \def\z@env{\global\z@firstlinetrue\z@changesize
  1011.     $$\z@inenvtrue\baselineskip\zedbaselineskip
  1012.     \parskip=0pt\lineskip=0pt\z@narrow
  1013.     \advance\displayindent by \zedindent
  1014.         \def\\{\crcr}% Must have \def and not \let for nested alignments.
  1015.         \everycr={\noalign{\ifz@firstline \global\z@firstlinefalse
  1016.                 \else \penalty\interzedlinepenalty \fi}}
  1017.         \tabskip=0pt}
  1018. \def\endz@env{$$\global\@ignoretrue}
  1019. %
  1020. % z lines are formated in two (overlaping) columns;
  1021. %    the first flush left having the same width as the environment,
  1022. %    and, the second flush right ending at the right end of the environment.
  1023. %
  1024. \def\z@format{\halign to\linewidth\bgroup%
  1025.         \zstrut\z@left\z@startline\ignorespaces$\@lign##$\z@stopline\hfil%
  1026.         \tabskip=0pt plus1fil%
  1027.         &\hbox to 0pt{\hss\@lign##}\tabskip=0pt\cr}
  1028. %
  1029. \def\z@boxenv{\z@narrow\let\also=\als@ \let\Also=\Als@ \let\ALSO=\ALS@
  1030.     \z@inboxtrue \predisplaypenalty=\preboxpenalty \z@env\z@format}
  1031. %
  1032. \def\z@outnonbox{\z@outclasscheck\z@leavevmode\z@env}
  1033. \def\z@inoutbox{\z@leavevmode\z@makeouter\z@inclassfalse\z@boxenv}
  1034. %
  1035. %    SPACING COMMANDS
  1036. %
  1037. % no vertical glue between abutted lines
  1038. %
  1039. \def\@but{\noalign{\nointerlineskip}}
  1040. %
  1041. % no \par extra vertical spacing after Z environments
  1042. %
  1043. %\def\z@nopar{\ifz@inclass\else\vskip-\parskip\fi}
  1044. %\def\z@nopar{\global\parskip0pt\global\everypar{\parskip30mm\everypar{}}}
  1045. \def\z@nopar{\global\@endpetrue}
  1046. %
  1047. % \z@leavevmode -- Enter horizontal mode, taking account of possible
  1048. % interaction with lists and section heads:
  1049. %
  1050. %    1    After a \item, use \indent to get the label (this
  1051. %        fails to run in even short labels).
  1052. %    2    After a run-in heading, use \indent.
  1053. %    3    After an ordinary heading, throw away the \everypar
  1054. %        tokens, reset \@nobreak, and use \noindent with \parskip
  1055. %        zero.
  1056. %    4    Otherwise, use \noindent with \parskip zero
  1057. %
  1058. % use when entering displayed environments to get correct spacing
  1059. %
  1060. \def\z@leavevmode{\ifvmode\if@inlabel\indent\else\if@noskipsec\indent\else
  1061.     \if@nobreak\global\@nobreakfalse\everypar={}\fi
  1062.     {\parskip=0pt\noindent}\fi\fi\fi}
  1063. %
  1064. % extra vertical space in non-box environments
  1065. %
  1066. \def\also{\crcr\noalign{\vskip\jot}}
  1067. \def\Also{\crcr\noalign{\vskip2\jot}}
  1068. \def\ALSO{\Also\Also}
  1069. %
  1070. % extra vertical space in boxed environments
  1071. %
  1072. \def\als@{\crcr\@but\omit\vrule height\jot width\zedlinethickness \cr \@but}
  1073. \def\Als@{\crcr\@but\omit\vrule height2\jot width\zedlinethickness \cr \@but}
  1074. \def\ALS@{\crcr\@but\omit\vrule height4\jot width\zedlinethickness \cr \@but}
  1075. %
  1076. %    ENVIRONMENT-BREAKING COMMANDS
  1077. %
  1078. \def\znewpage{\also\noalign{\penalty\forcepagepenalty}\also}
  1079. \def\zbreak{\also\noalign{\penalty\interdisplaylinepenalty\vskip-\jot}\also}
  1080. \def\Zbreak{\also\noalign{\penalty\interdisplaylinepenalty}\also}
  1081. \def\ZBREAK{\Also\noalign{\penalty\interdisplaylinepenalty}\Also}
  1082. %
  1083. \def\t#1{\hskip #1\zedtab}
  1084. \def\c#1#2{\hbox to #1\zedtab{$#2$\hfil}}
  1085. \def\flushr#1{\crcr\quad\cr}
  1086. %
  1087. %        ------ UTILITY MACROS FOR OBJECT-Z ------
  1088. %
  1089. \def\z@inclasscheck{\ifz@inclass\else
  1090.     \@latexerr{This Z environment is only allowed within a class}
  1091. {Perhaps you forgot to include a \string\begin\string{class\string}
  1092. somewhere^^Jor you are trying to print a file that needs updating.^^J\@ehc} \fi}
  1093. \def\z@outclasscheck{\ifz@inclass
  1094.     \@latexerr{This Z environment is not allowed inside a class}
  1095. {This environment doesn't really make sense within a class.^^J%
  1096. If you really want it then I'll try my best to fit in in.^^J\@ehc}\else
  1097. \ifz@inenv \@latexerr{New Z environment declared before previous
  1098. one is completed}
  1099. {I suspect that you've forgotten to finish the last environment.^^J%
  1100. You are trying to nest environments and this can only be done inside classes^^J%
  1101. besides, the environment you have started isn't valid within classes any way.^^JI suggest that you type \space X <return> \space to quit and then correct your document.}
  1102. \fi\fi}
  1103. %
  1104. \def\z@makeouter{\ifz@inenv\ifz@inclass\z@inenvfalse
  1105.     \hskip-\zedleftsep \advance\linewidth by -\zedlinethickness
  1106.     \zedindent=\zedleftsep \zedleftsep=0.8\zedleftsep
  1107.     \zedbar=0.8\zedbar \zedtab=0.8\zedtab
  1108.     \parbox[b]{\linewidth}\bgroup\z@zeroskips
  1109.     \else\@latexerr{Incorrect place for Z environment; nesting is
  1110. allowed only inside classes}
  1111. {You've either forgotten to finish the last environment,^^J%
  1112. you've forgotten to include a \string\begin\string{class\string} somewhere^^J%
  1113. or you are trying to print a file that needs updating.^^J%
  1114. (Then again, you might just be trying to do something^^J%
  1115. that the author of these macros didn't intend you to do)^^J\@ehc}
  1116.     \fi\else\bgroup\fi}
  1117. %
  1118. \def \z@makeinner{\egroup%
  1119. \global\z@curindent\z@}
  1120. %
  1121. \def \classbreak{\also\egroup$$\vskip -\ht\zstrutbox
  1122.     \vskip -\abovedisplayskip\vskip -\belowdisplayskip\z@wide\z@boxenv\also}
  1123. %
  1124. %        ------ NON-BOX ENVIRONMENTS ------
  1125. %
  1126.  
  1127. %
  1128. %    ZED            for non-box multiline formulas
  1129. %
  1130. \def\zed{\z@outnonbox\z@inboxfalse\z@format}
  1131. \def\endzed{\crcr\egroup\endz@env}
  1132. \let\[=\zed
  1133. \def\]{\crcr\egroup$$\ignorespaces}
  1134. %
  1135. %    ARGUE            for algebraic arguments
  1136. %
  1137. %    used for algebraic proofs expressed as extended equations.
  1138. %    like zed but with extra spacing between lines
  1139. %    Generates an alignment display, which may be split across pages.
  1140. %
  1141. \def\argue{\z@outnonbox\interzedlinepenalty=\interdisplaylinepenalty
  1142.     \openup 1\jot \z@format
  1143.     \noalign{\vskip-\jot}}% equal vspace above and below argue display
  1144. \let\endargue=\endzed
  1145. %
  1146. %    INFRULE            for inference rules
  1147. %
  1148. %    used for inference rules. The horizontal line is generated by \derive:
  1149. %    an optional argument contains the side-conditions of the rule.
  1150. %
  1151. \def\infrule{\z@outnonbox\halign\bgroup
  1152.     \zstrut\quad$\@lign##$\quad\hfil&\quad\@lign##\hfil\cr}
  1153. \let\endinfrule=\endzed
  1154. \def\derive{\crcr\also\@but\omit\z@hrulefill%
  1155.     \@ifnextchar[{\z@sidecondition}{\cr\also\@but}}
  1156. \def\Derive{\crcr\also\@but\omit\z@hrulefill\cr\@but
  1157.         \noalign{\kern-\dp\zstrutbox
  1158.     \kern\doublerulesep \nobreak}%
  1159. \omit\derive}
  1160. \def\z@sidecondition[#1]{&$\smash{\lower 0.2ex\hbox{$[\;#1\;]$}}$\cr\also\@but}
  1161. %
  1162. %    SYNTAX            for syntax rules
  1163. %
  1164. % `syntax' environment: used for syntax rules - even (once!) for VDM.
  1165. \def\syntax{\z@outnonbox\halign\bgroup
  1166.     \zstrut$\@lign##$\hfil &\hfil$\@lign{}##{}$\hfil
  1167.     &$\@lign##$\hfil &\qquad\@lign-- ##\hfil\cr}
  1168. \let\endsyntax=\endzed
  1169.  
  1170. %
  1171. %        ------ BOXED ENVIRONMENTS ------
  1172. %
  1173. %
  1174. %    SCHEMA            schema definitions
  1175. %
  1176. \def\schema#1{\z@inoutbox\z@topline{$\,#1\,$}}
  1177. \def\endschema{\z@botline \endzed \z@makeinner \z@nopar}
  1178. %
  1179. %    SCHEMA*            schema with no name
  1180. %
  1181. \@namedef{schema*}{\leftnamesfalse\z@inoutbox\z@topline{}}
  1182. \expandafter\let\csname endschema*\endcsname=\endschema
  1183. %
  1184. %    GENSCHEMA        generic schema definitions
  1185. %
  1186. \def\genschema#1#2{\z@inoutbox\z@topline{$\,#1\:[#2]\,$}}
  1187. \let\endgenschema=\endschema
  1188. %
  1189. %    AXDEF            'liberal' axiomatic definitions
  1190. %
  1191. \def\axdef{\z@inoutbox}
  1192. \def\endaxdef{\endzed\z@makeinner}
  1193. %
  1194. %    UNIQDEF            'unique' axiomatic definitions
  1195. %
  1196. \def\uniqdef{\leftnamesfalse\z@inoutbox\z@dbltopline{}}
  1197. \let\enduniqdef=\endschema
  1198. %
  1199. %    GENDEF            'generic' axiomatic definitions
  1200. %
  1201. \def\gendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}}
  1202. \let\endgendef=\endschema
  1203. %
  1204. %    CLASS
  1205. %
  1206. \def\class#1{\z@leavevmode\z@makeouter\z@inclasstrue
  1207.         \z@boxenv\z@topline{$\,#1\,$}}
  1208. \let\endclass\endschema
  1209. %
  1210. %    OP
  1211. %
  1212. \def\op{\z@inclasscheck\schema}
  1213. \let\endop\endschema
  1214. %
  1215. %    STATE
  1216. %
  1217. \def\state{\z@inclasscheck\vbox\bgroup\vskip-\ht\zstrutbox\vbox\bgroup\hbox\bgroup\@nameuse{schema*}}
  1218. \def\endstate{\endschema\egroup\egroup\egroup}
  1219. %
  1220. %    INIT
  1221. %
  1222. \def\init{\z@inclasscheck\schema{\Init}}
  1223. \let\endinit\endschema
  1224. %
  1225. %        ------ OTHER ENVIRONMENTS ------
  1226. %
  1227. %    SIDEBYSIDE
  1228. %
  1229. % This should support an arbitary number of columns
  1230. %    \zedindent's proportion of \linewidth gives a practical limit
  1231. %
  1232. \def\sidebyside{\@ifnextchar[{\z@columns}{\z@columns[2]}}
  1233. \def\z@columns[#1]{\z@leavevmode\z@cols#1 \z@makeouter\z@narrow%
  1234.     $$\lineskip=0pt\z@incolstrue
  1235.     \predisplaysize\maxdimen
  1236.     \ifz@leftmargin\hskip-\zedindent\z@leftmarginfalse\fi
  1237.     \setbox0=\hbox to \linewidth\bgroup\z@zeroskips%
  1238.     \divide\zedbar by \z@cols \divide\zedleftsep by \z@cols
  1239.     \divide\zedtab by \z@cols \divide\linewidth by \z@cols
  1240.     \parbox[t]{\linewidth}\bgroup\z@wide}
  1241. %
  1242. \def\nextside{\egroup\hss\parbox[t]{\linewidth}\bgroup\z@wide}
  1243. %
  1244. \newdimen\z@temp
  1245. \def\endsidebyside{\egroup\egroup
  1246.     \z@temp\ht0 \advance\z@temp by \dp0\advance\z@temp by-\dp\zstrutbox
  1247.     \hbox{\raise\z@temp\box0}\endz@env\z@makeinner\z@nopar}
  1248. %
  1249. %    ZPAR
  1250. %
  1251. \def\zpar{\z@leavevmode
  1252.     \ifz@inenv\z@inclasstrue\fi% fudge to let zpar in all boxes
  1253.     \z@makeouter\z@changesize
  1254.     \advance\linewidth by -\z@curindent
  1255.     \advance\linewidth by -\wd\z@curline
  1256.     \hskip-\wd\z@curline\advance\linewidth by -\zedindent$$
  1257.     \ifz@leftmargin\hskip-\zedindent\fi% adjustment for first column
  1258.     \advance\displayindent by \zedindent
  1259.     \advance\displaywidth by -\zedindent
  1260.     \advance\displayindent by \z@curindent
  1261.     \advance\displayindent by \wd\z@curline
  1262.     \advance\displaywidth by -\z@curindent
  1263.     \advance\displaywidth by -\wd\z@curline
  1264.     \global\setbox\z@curline\hbox{}
  1265.     \z@narrow\parbox[b]{\linewidth}\bgroup\hfil\break}
  1266. \def\endzpar{\egroup$$\z@makeinner\z@nopar}
  1267. %
  1268. %    CLASSCOM
  1269. %
  1270. \def \classcom{\zpar\sf}
  1271. \let \endclasscom=\endzpar
  1272. %
  1273. %    PROOF
  1274. %
  1275. \def\proof{\zpar$\PR$\zpar}
  1276. \def\endproof{\endzpar\endzpar}
  1277. %
  1278. % Additional auxiliary macros
  1279. %
  1280. \def\zseq#1{\lseq #1 \rseq}
  1281. \def\zset#1{\{ #1 \}}
  1282. \def\zimg#1{\limg #1 \rimg}
  1283. \def\zsch#1{\lsch #1 \rsch}
  1284. \def\zimgset#1{\zimg\zset{#1}}
  1285. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  1286. %%%%%
  1287. %%%%%        FUTURE UPDATES:
  1288. %%%%%
  1289. %%%%% investigate the setting of \par to minimise space after schemas & zpars
  1290. %%%%% make display skips bigger for large fonts
  1291. %%%%%
  1292. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  1293.